Lemmas | fpf wf, Knd wf, Id wf, fpf-compatible wf, Rframe wf, decl-type wf, rationals wf, fpf-join wf, decl-state wf, ma-valtype wf, fpf-cap-single1, fpf-single wf3, id-deq wf, fpf-compatible-join-cap, fpf-cap-join-subtype, subtype rel self, top wf, fpf-cap wf, subtype rel dep function, l member wf, Reffect wf, Rall wf, Rplus wf |